A, B:Realizer. A || B  (i:Id. R-ds(A;i) || R-ds(B;i)) 

latex

Definitions

, Realizer, AB, P  Q, A || B, x:A. B(x), f || g, Id, Type, IdDeq, R-ds(R;i), n+m, R-size(R), n-m, -n, ij, , A, False, Void, a<b, #$n, x:AB(x), {x:A| B(x) }, t  T, , P  Q, left+right, s ~ t, SQType(T), {T}, P  Q, P & Q, x:AB(x), Rplus?(x1), Prop, s = t, , b, b, es realizer ind Rplus compseq tag def, f  g, x. t(x), x.A(x), Rplus-left(x1), Rplus-right(x1), Rnone?(x1), es realizer ind Rnone compseq tag def, x:A. B(x), a:A fp B(a), Top, x(s), f(a), EqDecider(T), T, P  Q, True, Atom$n, if b t else f fi, , Unit, a = b, R-loc(R), Rds(R)

Lemmas

Rds wf, R-loc wf, eq id wf, assert-eq-id, not functionality wrt iff, fpf-empty wf, ifthenelse wf, Id sq, R-ds-Rds, deq wf, true wf, squash wf, fpf-compatible wf, fpf-empty-compatible-right, top wf, fpf wf, fpf-trivial-subtype-top, fpf-empty-compatible-left, Rnone-implies, Rnone? wf, Rplus-right wf, Rplus-left wf, R-compat-symmetry, R-ds wf, id-deq wf, fpf-compatible-join, fpf-join wf, fpf-compatible-symmetry, R-size-decreases, Rplus-implies, assert wf, not wf, bnot wf, bool wf, Rplus? wf, assert of bnot, eqff to assert, iff transitivity, bool sq, eqtt to assert, bool cases, nat plus wf, R-size wf, le wf, es realizer wf, R-compat wf, Id wf, nat wf, nat properties, ge wf